package preprocessor.absorption;

import kb.*;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import option.KBVocabulary;

import entities.concept.AndConcept;
import entities.concept.AtomicConcept;
import entities.concept.Concept;
import entities.concept.NotConcept;
import entities.concept.OrConcept;
//import entities.concept.PConcept;

import tableaux.Completion;
import utils.exception.ConceptException;
import preprocessor.Simplification;

/**
 * Concept absorption needs to consider negated absorption and enhanced
 * absorption as well. In addition, we impose that concept absorption has higher
 * priority than binary absorption in the sense that given A=>.., B=>..., binary
 * absorption has to consider if it is possible to absorb (A and B) => X This is
 * the same as Enhanced concept absorption problem, i.e., not (A and B)=>Y
 * enforces the addition of Top => X or Y.
 * 
 * This is now not a constrain on concept absorption, rather one on binary
 * absorption. i.e., binary absorption is given lower priority than concept
 * absorption.
 * 
 * @see Absorption
 * 
 * @author j55wu
 * 
 */
public class UnaryAbsorption implements Absorption {

	private TBox tbox;

	public static enum CA_ORDER {
		CA_FIRST, NCA_FIRST
	};

	private CA_ORDER order;

	public UnaryAbsorption(TBox tb, CA_ORDER od) {
		this.tbox = tb;
		this.order = od;
		if (!Absorption.NCA && this.order.equals(CA_ORDER.NCA_FIRST)) {
			System.err
					.println("Negated unary absorption is preferred, but it is disallowed... Order ignored.");
			this.order = CA_ORDER.CA_FIRST;
		}
	}

	/**
	 * Given a set of general axioms, with references to Tu, Tnu, Tb and other
	 * possible sub-Tboxes, the absorption must be able to classify GCIs into
	 * appropriate sub-Tboxes.
	 * 
	 * This method absorbs axioms in Tg.
	 */
	public boolean absorb() {
		//
		boolean suc = false;
		if (this.tbox.getTg().size() > 0) {
			Set<Concept> cs = new HashSet<Concept>();
			Set<Concept> remain = new HashSet<Concept>();
			Set<Concept> topadded = new HashSet<Concept>();
			boolean topChanged = false;
			for (Concept c : this.tbox.getTg().keySet()) {
				Concept rhs = this.tbox.getTg().get(c);
				if (c.isTop()) {
					// top -> C1 and C2 and ... and Cn, absorb Ci separately.
					for (Concept each : Concept.reduceToConjuncts(rhs)) {
						boolean part = this.applyConceptAbsorption(
								Concept.reduceToDisjuncts(each), this.order);
						if (!part) {
							topadded.add(each);
						} else {
							// System.err.println("absorbed: top-> "+each);
							topChanged = true;
							suc = true;
						}
					}
				} else if (absorbAxiom(c, rhs, this.order)) {
					cs.add(c);
					suc = true;
				} else {
					// not absorbed by the first method
					remain.add(c);
				}
			}
			// finished the preferred absorption, now apply the low-priority one
			// to remaining axioms
			CA_ORDER otherOd = null;
			if (this.order.equals(CA_ORDER.CA_FIRST)) {
				otherOd = CA_ORDER.NCA_FIRST;
			} else if (this.order.equals(CA_ORDER.NCA_FIRST)) {
				otherOd = CA_ORDER.CA_FIRST;
			}
			boolean secondAbs = true;
			if (otherOd.equals(CA_ORDER.NCA_FIRST) && !Absorption.NCA) {
				secondAbs = false;
			}
			if (secondAbs) {
				for (Concept cc : remain) {
					Concept rhs = this.tbox.getTg().get(cc);
					boolean fur = absorbAxiom(cc, rhs, otherOd);
					if (fur) {
						suc = true;
						cs.add(cc);
					}
				}
			}
			for (Concept cc : cs) {
				this.tbox.getTg().remove(cc);
			}
			if (secondAbs) {
				Set<Concept> rmed = new HashSet<Concept>();
				for (Concept toprhs : topadded) {
					boolean fur = this.applyConceptAbsorption(
							Concept.reduceToDisjuncts(toprhs), otherOd);
					if (fur) {
						topChanged = true;
						suc = true;
						rmed.add(toprhs);
					}
				}
				topadded.removeAll(rmed);
			}
			// modify top GCI
			if (topChanged) {
				if (topadded.size() == 1) {
					this.tbox.getTg().put(KBVocabulary.CONCEPT_TOP,
							topadded.iterator().next());
				} else if (topadded.size() > 1) {
					this.tbox.getTg().put(KBVocabulary.CONCEPT_TOP,
							new AndConcept(topadded));
				} else {
					// remove this top GCI
					this.tbox.getTg().remove(KBVocabulary.CONCEPT_TOP);
				}
			}
		}
		return suc;
	}

	public boolean absorbAxiom(Concept l, Concept r, CA_ORDER od) {
		boolean suc = false;
		if (l == null) {
			return suc;
		}
		HashSet<Concept> cons = new HashSet<Concept>();
		cons.add(r);
		cons.add(Simplification.NNF(new NotConcept(l), false));
		suc = this.applyConceptAbsorption(
				Concept.reduceToDisjuncts(new OrConcept(cons)), od);
		return suc;
	}

	// public boolean absorbAxiom(InclusionAxiom ax){
	// boolean suc = false;
	// if(ax == null){
	// return suc;
	// }
	// //if LHS is already a named concept.
	// if(ax.getLHS().isAtomic()){
	// try{
	// this.tbox.insertTu(ax);
	// }catch(Exception e){
	// e.printStackTrace();
	// }
	// }else{
	// //get disjuncts
	// suc = this.applyConceptAbsorption(Axiom.axiomToDisjuncts(ax));
	// //make decisions about how to absorb here
	// }
	// return suc;
	// }

	private boolean applyConceptAbsorption(HashSet<Concept> dis, CA_ORDER od) {
		boolean suc = false;
		for (Concept c : dis) {
			if (Absorption.CA && od.equals(CA_ORDER.CA_FIRST)) {
				if (c.isSimpleNot()) {
					suc = absorbPositiveConcept(dis, c);
					if (suc) {
						return true;
					}
				}
			} else if (Absorption.NCA && od.equals(CA_ORDER.NCA_FIRST)) {
				if (c instanceof AtomicConcept) {
					suc = absorbNegatedConcept(dis, c);
					if (suc) {
						return true;
					}
				}
			}
		}
		return suc;
	}

	private boolean absorbPositiveConcept(HashSet<Concept> dis, Concept c) {
		NotConcept nc = (NotConcept) c;
		AtomicConcept pc = (AtomicConcept) nc.getConcept();
		// decide if Negated concepts matters!
		if (Absorption.NCA && tbox.getTnu().containsKey(nc)) {
			// consider if enhanced concept absorption allowed
			// ~A=>C1 A=>C2, then Top=>C1 or C2
			if (Absorption.ECA) {
				// absorb and add an extra GCI...
				Concept c1 = tbox.getTnu().get(nc);
				HashSet<Concept> disnew = new HashSet<Concept>();
				disnew.addAll(dis);
				disnew.remove(c);
				try {
					tbox.insertTu(pc, new OrConcept(disnew));
				} catch (ConceptException e) {
					e.printStackTrace();
				}
				// add an extra GCI
				disnew.add(c1);
				Concept c2 = new OrConcept(disnew);
				tbox.saveGeneratedGCIs(KBVocabulary.CONCEPT_TOP, c2);
				return true;
			} else {
				return false;
			}
		} else {
			// there is no competition considered: first come first serve~~
			// so the order of concepts in a set really matters~ and absorption
			// may give different results.
			HashSet<Concept> disnew = new HashSet<Concept>();
			disnew.addAll(dis);
			disnew.remove(c);
			// System.out.println("Unary absorpotion: "+pc+" -> "+disnew);
			Concept arhs = null;
			if (disnew.size() == 1) {
				arhs = disnew.iterator().next();
			} else {
				arhs = new OrConcept(disnew);
			}
			try {
				tbox.insertTu(pc, arhs);
				return true;
			} catch (ConceptException e) {
				e.printStackTrace();
			}

		}
		return false;
	}

	private boolean absorbNegatedConcept(HashSet<Concept> dis, Concept c) {
		// negated concept absorption
		boolean suc = false;
		NotConcept nc = new NotConcept(c);
		if (tbox.getTu().containsKey(c)) {
			// consider if enhanced concept absorption allowed
			// A=>C1 ~A=>C2, then Top=>C1 or C2
			if (Absorption.ECA) {
				Concept c1 = tbox.getTu().get(c);
				HashSet<Concept> disnew = new HashSet<Concept>();
				disnew.addAll(dis);
				disnew.remove(c);
				try {
					tbox.insertTnu(nc, new OrConcept(disnew));
				} catch (ConceptException e) {
					e.printStackTrace();
				}
				// add an extra GCI
				disnew.add(c1);
				Concept c2 = new OrConcept(disnew);
				tbox.saveGeneratedGCIs(KBVocabulary.CONCEPT_TOP, c2);
				suc = true;// because new GCI generated
				return true;
			} else {
				return false;
			}
		} else {
			// ~A -> C added directly, no GCIs added
			HashSet<Concept> disnew = new HashSet<Concept>();
			disnew.addAll(dis);
			disnew.remove(c);
			Concept arhs = null;
			if (disnew.size() == 1) {
				arhs = disnew.iterator().next();
			} else {
				arhs = new OrConcept(disnew);
			}
			try {
				tbox.insertTnu(nc, arhs);
				suc = true;
			} catch (ConceptException e) {
				e.printStackTrace();
			}
			// resolution to binary axioms, e.g., {a} and DEF_R -> some R.xxx
			// ~DEF_R->C
			// then must be the case {a} -> some R.xxx or C
			AtomicConcept pc = (AtomicConcept) c;
			if (!suc) {
				return false;
			}
			if (BinaryAbsorptionGuarded.defOrder
					.equals(BinaryAbsorptionGuarded.entryOrder.Nominal_Second)) {
				Map<AtomicConcept, Map<AtomicConcept, Concept>> bas = tbox
						.getSpecialBinaryClass().getTbLimited();
				if (bas.containsKey(pc)) {
					Map<AtomicConcept, Concept> ins = bas.get(pc);
					for (AtomicConcept o : ins.keySet()) {
						Concept newor = new OrConcept(ins.get(o), arhs);
						try {
							tbox.insertTu(o, newor);
							Completion.nominalInTu = true;
							// System.out.println("extra: "+o+"->"+newor);
						} catch (ConceptException e) {
							e.printStackTrace();
						}
					}
				}

			} else {
				System.err
						.println("To be implemented: negated CA and bianry entries absortion failed, quitting system~~");
				System.exit(-1);
			}
		}
		return suc;
	}

}
